Inference at * 1 3 1 0 2 1 2 
Iof proof for Lemma fincr wf:

.....set predicate..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
  0  (n+1) 

latex

 by Arith 

latex

 1: .....wf..... NILNIL

 1: 3. n : 
 1: 4. 0  n
 1:   n+1  
 2: .....wf..... NILNIL

 2: 3. n : 
 2: 4. 0  n
 2:   0  
 .

Definitions

s = t, #$n, f(a), x:A. B(x), , {x:A| B(x)} , , x:AB(x), Void, a < b, n+m, , t  T, False, P  Q, A, A  B